Kleisli TripleとMonadの対応
table:対応
クライスリトリプル Haskell
T 型コンストラクタM
η return
(-)^* (=<<) 反対向きのbind
Monad型クラスの定義
code:hs
class Applicative m => Monad (m :: * -> *) where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a
また、(=<<)は、(>>=)の2つの引数を入れ替えたものなので、
型は、(a -> m b) -> m a -> m b
クライスリトリプル
①$ f^*\circ\eta_A=f
②$ \eta_A^*=\mathrm{id}_{TA}
③$ g^*\circ f^*=(g^*\circ f)^*
モナド則
code:hs
return x >>= f == f x -- ①
m >>= return == m -- ②
(m >>= f) >>= g == m >>= (\x -> f x >>= g) -- ③
前提
code:hs
return :: A -> M A
f :: A -> B
g :: B -> C
コツは、
Monad型クラスでよく定義される(>>=)と向きが逆であることに注意すること
Monad型クラスの方を(=<<)に変換してから考えるとわかりやすくなる
ポイントフリーにしてる感じ
なので良い感じに引数を与えてあげるとHaskellとの対応が取りやすくなる
モナド則のxとかmはどこから来たの？という感じなので、例えば①も\x -> return x >>= fのように、xを引数として与えるように書き直せば扱いやすくなる
①の対応
$ f^*\circ\eta_A=fの左辺をそのままHaskellで書くと、
(=<<) f . returnになる
この型は、A -> Bである
これのbindの向きを変えて、>>=を使うように変更すると、
(\x -> x >>= f) . returnと書ける
合成.の仕方を考えれば、これは(\x -> return x >>= f)と同じであることがわかる
これで、両者の左辺$ f^*\circ\eta_Aとreturn x >>= fの対応が取れた
右辺も同じで、ちゃんと書けば\x -> f xなので、対応が取れている
図で見るとわかりやすい
https://gyazo.com/b7264cf0fb6a3de93633f7e9b2fcae4b
②の対応
$ \eta_A^*=\mathrm{id}_{TA}の左辺をそのままHaskellで書くと、
(=<<) returnになる
この型は、M A -> M A
これのbindの向きを変えて、>>=を使うように変更すると、
\m -> (=<<) return m
\m -> (>>=) m return
\m -> m >>= return
これは、モナド則の2つ目の左辺と同じである
右辺もmを与えてあげるようにすれば、
\m -> id mであり、これはモナド則の右辺と同じ
https://gyazo.com/ef7543f186ad1dfe3ec86b2abed3613b
③の対応
$ g^*\circ f^*=(g^*\circ f)^*の左辺と右辺を別々に変換していって、モナド則と同じ形にする
まず左辺を見る
$ g^*\circ f^*をそのままHaskellで書くと
(=<<) g . (=<<) f
(\m -> (=<<) g m) . (=<<) f
gの方をポイントフリーでなくしたmrsekut.icon
(\m -> m >>= g) . (=<<) f
gの方で>>=を使うように書き換えたmrsekut.icon
\m -> (=<<) f m >>= g
\m -> m >>= f >>= g
これで、モナド則の左辺と同じになった
右辺
$ (g^*\circ f)^*をそのままHaskellで書くと、
(=<<) ((=<<) g . f)
(=<<) ((\x -> (=<<) g x) . f)
gの方をポイントフリーでなくしたmrsekut.icon
(=<<) ((\x -> x >>= g) . f)
gの方で>>=を使うように書き換えたmrsekut.icon
(=<<) (\x -> f x >>= g)
\m -> (=<<) (\x -> f x >>= g) m
\m -> m >>= (\x -> f x >>= g)
これで、モナド則の右辺と同じになった